T:Type, L1, L2:T List. interleaving(T;L1;L2;nil)  L1 = nil & L2 = nil 

latex

Definitions	t  T, Prop, P & Q, interleaving(T;L1;L2;L), x:A. B(x), P  Q, P  Q, P  Q, ||as||, ij
Lemmas	nil interleaving, length interleaving, non neg length, length wf1, length zero, interleaving wf